Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(group_theory/noncomm_pi_coprod): homomorphism from pi monoids or groups #11744

Closed
wants to merge 148 commits into from
Closed

[Merged by Bors] - feat(group_theory/noncomm_pi_coprod): homomorphism from pi monoids or groups #11744

wants to merge 148 commits into from

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Jan 31, 2022 •
edited by semorrison

Co-authored-by: Junyan Xu junyanxumath@gmail.com

@alreadydone wrote on zulip:

It may be worth doing the following: given a family of homomorphisms Hi -> G into the same group, if the ranges of any two different homomorphisms commute, then we get a canonical homomorphism from a subgroup of the pi group of the Hi's (with finitely many components non-identity), or alternatively from a quotient group (by the commutators between different Hi's) of the free_product, into G. Then we can state that this canonical homomorphism is an isomorphism, and it will be a Prop.

This nerd-sniped me, and suddenly it is past 2am, but here it is:

  • The construction of the homomorphism
  • A lemma about its range
  • Injectivity if the ranges are complete_lattice.independent
  • The mul_equiv statement in the latter case.

I restricted myself to case of finitely many groups.

I plan to use this in #nilpotent. But I expect this will need thorough cleanup:

  • Where this should go
  • namespacing and naming
  • lots of code golfing,
  • maybe partial rewrite
  • documentation

So it’s a draft for now. But do fire away!

No longer a draft, but cleaned up and documented. Now less ashamed of it :-)

Open in Gitpod

@nomeata nomeata mentioned this pull request Jan 31, 2022
Closed
45 tasks
@nomeata
Copy link
Collaborator Author

nomeata commented Feb 1, 2022

I have greatly reworked this file:

  • Included a module header that should explain things.
  • Sorted definitions into appropriate namespaces. First all the S-restricted stuff, then the main stuff.
  • Generalized some of the lemmas about independent subgroups.

@nomeata nomeata marked this pull request as ready for review February 1, 2022 14:28
nomeata
nomeata commented Feb 1, 2022
View reviewed changes
src/group_theory/pi_hom.lean Outdated Show resolved Hide resolved
src/group_theory/pi_hom.lean Outdated Show resolved Hide resolved
src/group_theory/pi_hom.lean Outdated Show resolved Hide resolved
src/group_theory/pi_hom.lean Outdated Show resolved Hide resolved
@nomeata nomeata added the awaiting-review The author would like community review of the PR label Feb 1, 2022
nomeata
nomeata commented Feb 1, 2022
View reviewed changes
src/group_theory/pi_hom.lean Outdated Show resolved Hide resolved
@jcommelin

This comment was marked as resolved.

Sign in to view
@nomeata nomeata mentioned this pull request Mar 12, 2022
Closed
2 tasks
nomeata and others added 2 commits March 12, 2022 21:28
@nomeata
Use pi.mul_single_apply_commute
92719f4
@nomeata @jcommelin
Apply suggestions from code review
bf98c60 
Co-authored-by: Johan Commelin <johan@commelin.net>
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Mar 14, 2022
@leanprover-community-bot-assistant
Copy link
Collaborator

This PR/issue depends on:

@nomeata nomeata added awaiting-review The author would like community review of the PR and removed merge-conflict Please `git merge origin/master` then a bot will remove this label. labels Mar 14, 2022
@nomeata
Copy link
Collaborator Author

nomeata commented Mar 14, 2022

The yak that was shaved at #11744 two weeks ago came back after, and now this PR is again on the top of the stack towards the finite nilpotency equivalences.

@semorrison semorrison added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Mar 15, 2022
@nomeata @semorrison
fix partly embarrassing typos
9197315 
Co-authored-by: Scott Morrison <scott@tqft.net>
@nomeata nomeata added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Mar 15, 2022
@semorrison
Copy link
Collaborator

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Mar 16, 2022
bors bot pushed a commit that referenced this pull request Mar 16, 2022
@nomeata @alreadydone
feat(group_theory/noncomm_pi_coprod): homomorphism from pi monoids or…
717b11e 
… groups (#11744)

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>



Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
@bors
Copy link

bors bot commented Mar 16, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(group_theory/noncomm_pi_coprod): homomorphism from pi monoids or groups [Merged by Bors] - feat(group_theory/noncomm_pi_coprod): homomorphism from pi monoids or groups Mar 16, 2022
@bors bors bot closed this Mar 16, 2022
@bors bors bot deleted the joachim/pi_nom branch March 16, 2022 13:40
laurentbartholdi pushed a commit that referenced this pull request Mar 17, 2022
@nomeata @alreadydone @laurentbartholdi
feat(group_theory/noncomm_pi_coprod): homomorphism from pi monoids or…
5f9b4c8 
… groups (#11744)

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>



Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@semorrison semorrison semorrison left review comments

@alreadydone alreadydone alreadydone left review comments

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@nomeata @jcommelin @alreadydone @leanprover-community-bot-assistant @semorrison @eric-wieser